|
In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of clauses, where a clause is a disjunction of literals; otherwise put, it is an AND of ORs. As a normal form, it is useful in automated theorem proving. It is similar to the product of sums form used in circuit theory. All conjunctions of literals and all disjunctions of literals are in CNF, as they can be seen as conjunctions of one-literal clauses and conjunctions of a single clause, respectively. As in the disjunctive normal form (DNF), the only propositional connectives a formula in CNF can contain are and, or, and not. The not operator can only be used as part of a literal, which means that it can only precede a propositional variable or a predicate symbol. In automated theorem proving, the notion "''clausal normal form''" is often used in a narrower sense, meaning a particular representation of a CNF formula as a set of sets of literals. ==Examples and non-examples== All of the following formulas in the variables A, B, C, D, and E are in conjunctive normal form: * * * * The last formula is in conjunctive normal form because it can be seen as the conjunction of the two single-literal clauses and . Incidentally, the last two formulas are also in disjunctive normal form. The following formulas are ''not'' in conjunctive normal form: * * * Every formula can be equivalently written as a formula in conjunctive normal form. In particular this is the case for the three non-examples just mentioned; they are respectively equivalent to the following three formulas, which are in conjunctive normal form: * * * 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「conjunctive normal form」の詳細全文を読む スポンサード リンク
|